A, B:MsgA. (A ||+ B)  Feasible(A)  Feasible(B)  Feasible(A  B) 

latex

Definitions

x:A  B(x), a:A fp B(a), x:A.B(x), ma-frame-compatible(A;B), M1 || M2, A ||+ B, f(a), f(x), A, Dec(P), if b then t else f fi , xdom(f). v=f(x)   P(x;v), Atom$n, Id, False, t  T, P & Q, P  Q, x:A. B(x), A c B, case b of inl(x) => s(x) | inr(y) => t(y), left + right, P  Q, x:AB(x), Outcome, True, , {x:A| B(x)} , {i..j}, A  B, a < b, i  j < k, FinProbSpace, type List, *1*, x. t(x), , ||as||, Void, M1 ||decl M2, <a, b>, , P  Q, Unit, s ~ t, {T}, SQType(T), P  Q, f  g, b  dom(M.prob), a in dom(M.pre), M.da(a), ma-prob(M;b), ma-prob-da-dom(M;b), ma-prob-da(M), , IdDeq, IdLnk, product-deq(A;B;a;b), State(ds), t.1, rcv(l,tg), , t.2, , T, Valtype(da;k), mk-ma, MsgA, Feasible(M), KindDeq, Type, Knd, f || g, Top, locl(a), f(x)?z, s = t, x  dom(f), b, M1  M2, ma-frame-compat(A;B)

Lemmas

ma-join-frame-compat, ma-join wf, ma-join-frame-compat2, decidable wf, fpf-join-ap, fpf-join-dom, fpf-join-cap-sq, fpf-join-dom-sq, and functionality wrt iff, implies functionality wrt iff, assert of bor, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, length wf nat, fpf-cap wf